STM: divides wf

STM: comb for divides wf

STM: zero divs only zero

STM: one divs any

STM: any divs zero

STM: divides invar 1

STM: divides invar 2

STM: divisors bound

STM: only pm one divs one

STM: divides of absvals

STM: divides reflexivity

STM: divides transitivity

STM: divides preorder

STM: divides anti sym n

STM: divides anti sym

STM: assoc reln

STM: divisor of sum

STM: divisor of minus

STM: divisor of mul

STM: divides mul

STM: divisor bound

STM: divides iff rem zero

STM: divides iff div exact

STM: decidable divides

STM: divides instance

ABS: a ~ b

STM: assoced wf

STM: comb for assoced wf

STM: assoced equiv rel

STM: decidable assoced

STM: divides functionality wrt assoced

STM: divides weakening

STM: assoced weakening

STM: assoced transitivity

STM: multiply functionality wrt assoced

STM: assoced inversion

STM: assoced functionality wrt assoced

STM: assoced elim

STM: mul cancel in assoced

STM: neg assoced

STM: absval assoced

STM: unit chars

STM: assoced nelim

STM: pdivisor bound

STM: divides nchar

ABS: GCD(a;b;y)

STM: gcd p wf

STM: comb for gcd p wf

STM: gcd p functionality wrt assoced

STM: gcd p eq args

STM: gcd p zero

STM: gcd p one

STM: gcd p zero rel

STM: gcd p sym

STM: gcd p sym a

STM: gcd p neg arg

STM: gcd p neg arg a

STM: gcd p neg arg 2

STM: gcd p shift

STM: gcd unique

STM: gcd of triple

ABS: gcd(a;b)

STM: gcd wf

STM: comb for gcd wf

STM: gcd sat gcd p

STM: gcd sat pred

STM: gcd elim

STM: gcd sym

STM: gcd is divisor 1

STM: gcd is divisor 2

STM: gcd is gcd

STM: quot rem exists n

STM: quot rem exists

STM: gcd exists n

STM: gcd ex n

STM: gcd exists

STM: bezout ident n

STM: bezout ident

STM: gcd p mul

STM: gcd mul

STM: gcd assoc

ABS: CoPrime(a,b)

STM: coprime wf

STM: comb for coprime wf

STM: sq stable coprime

ABS: reducible(a)

STM: reducible wf

ABS: atomic(a)

STM: atomic wf

STM: atomic char

ABS: prime(a)

STM: prime wf

STM: self divisor mul

STM: prime imp atomic

STM: prime elim

STM: coprime intro

STM: coprime elim

STM: coprime elim a

STM: coprime iff ndivides

STM: coprime bezout id0

STM: coprime bezout id1

STM: coprime bezout id2

STM: coprime bezout id

STM: coprime prod

STM: coprime divisors prod

STM: atomic imp prime

STM: prime divs prod

ABS: a = b mod m

STM: eqmod wf

STM: comb for eqmod wf

STM: eqmod weakening

STM: eqmod transitivity

STM: eqmod inversion

STM: eqmod functionality wrt eqmod

STM: eqmod fun

STM: add functionality wrt eqmod

STM: multiply functionality wrt eqmod

STM: chrem exists aux

STM: chrem exists aux a

STM: chrem exists

STM: chrem exists a

ABS: fib(n)

STM: fib wf

STM: comb for fib wf

STM: fib coprime